firewire.false.jani:model: info: firewire.false is an MDP model.
firewire.false.jani:variables[7]: info: Expanding variable "s1" into 9 locations in automaton "node1".
firewire.false.jani:variables[8]: info: Expanding variable "w21" into 10 locations in automaton "wire21".
firewire.false.jani:variables[12]: info: Expanding variable "s2" into 9 locations in automaton "node2".
firewire.false.jani: info: Need 16 bytes per state.
firewire.false.jani: info: Explored 212268 states for delay=36, deadline=800.
firewire.false.jani: info: Bounded value iteration for property "deadline" has converged at bound 37.
Peak memory usage: 1248 MB
Analysis results for firewire.false.jani
Experiment delay=36, deadline=800
+ State space exploration
State size: 16 bytes
States: 212268
Transitions: 478752
Branches: 481788
Rate: 239310 states/s
Time: 0.9 s
+ Property deadline
Probability: 0
Bounds: [0, 0]
CDF: { (0, 0), ..., (37, 0) }
Time: 15.7 s
+ Essential states
Iterations: 3
Essential states: 210809
Transitions: 477281
Branches: 480317
Time: 0.1 s
+ State elimination
States: 195794
Transitions: 2418134
Branches: 7860282
Time: 15.2 s
+ Value iteration
Time: 0.4 s
Exported results to file "/out.txt".